H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 1.794 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ LR

mainModule Monad

((filterM :: Monad b => (a -> b Bool) -> [a] -> b [a]) :: Monad b => (a -> b Bool) -> [a] -> b [a])

module Monad where

import qualified Maybe
import qualified Prelude

filterM :: Monad a => (b -> a Bool) -> [b] -> a [b]

filterM	_ []	=	return []
filterM	p (x : xs)	=	p x >>= (\flg ->filterM p xs >>= (\ys ->return ( if flg then x : ys else ys)))

module Maybe where

import qualified Monad
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\ys→return (if flg then x : ys else ys)

is transformed to

filterM0 flg x ys = return (if flg then x : ys else ys)

The following Lambda expression

\flg→filterM p xs >>= filterM0 flg x

is transformed to

filterM1 p xs x flg = filterM p xs >>= filterM0 flg x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

mainModule Monad

((filterM :: Monad a => (b -> a Bool) -> [b] -> a [b]) :: Monad a => (b -> a Bool) -> [b] -> a [b])

module Maybe where

import qualified Monad
import qualified Prelude

module Monad where

import qualified Maybe
import qualified Prelude

filterM :: Monad a => (b -> a Bool) -> [b] -> a [b]

filterM	_ []	=	return []
filterM	p (x : xs)	=	p x >>= filterM1 p xs x

filterM0

flg x ys

return ( if flg then x : ys else ys)

filterM1

p xs x flg

filterM p xs >>= filterM0 flg x

If Reductions:
The following If expression

if flg then x : ys else ys

is transformed to

filterM00 x ys True = x : ys

filterM00 x ys False = ys

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

mainModule Monad

((filterM :: Monad b => (a -> b Bool) -> [a] -> b [a]) :: Monad b => (a -> b Bool) -> [a] -> b [a])

module Monad where

import qualified Maybe
import qualified Prelude

filterM :: Monad a => (b -> a Bool) -> [b] -> a [b]

filterM	_ []	=	return []
filterM	p (x : xs)	=	p x >>= filterM1 p xs x

filterM0

flg x ys

return (filterM00 x ys flg)

filterM00	x ys True	=	x : ys
filterM00	x ys False	=	ys

filterM1

p xs x flg

filterM p xs >>= filterM0 flg x

module Maybe where

import qualified Monad
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Monad

((filterM :: Monad a => (b -> a Bool) -> [b] -> a [b]) :: Monad a => (b -> a Bool) -> [b] -> a [b])

module Maybe where

import qualified Monad
import qualified Prelude

module Monad where

import qualified Maybe
import qualified Prelude

filterM :: Monad b => (a -> b Bool) -> [a] -> b [a]

filterM	vw []	=	return []
filterM	p (x : xs)	=	p x >>= filterM1 p xs x

filterM0

flg x ys

return (filterM00 x ys flg)

filterM00	x ys True	=	x : ys
filterM00	x ys False	=	ys

filterM1

p xs x flg

filterM p xs >>= filterM0 flg x

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                  ↳ Narrow

mainModule Monad

(filterM :: Monad a => (b -> a Bool) -> [b] -> a [b])

module Monad where

import qualified Maybe
import qualified Prelude

filterM :: Monad a => (b -> a Bool) -> [b] -> a [b]

filterM	vw []	=	return []
filterM	p (x : xs)	=	p x >>= filterM1 p xs x

filterM0

flg x ys

return (filterM00 x ys flg)

filterM00	x ys True	=	x : ys
filterM00	x ys False	=	ys

filterM1

p xs x flg

filterM p xs >>= filterM0 flg x

module Maybe where

import qualified Monad
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="filterM\n  Monad a",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="filterM vz3\n  Monad a",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="filterM vz3 vz4\n  Monad a",fontsize=16,color="burlywood",shape="triangle"];122[label="vz4/vz40 : vz41",fontsize=10,color="white",style="solid",shape="box"];4 -> 122[label="",style="solid", color="burlywood", weight=9];
122 -> 5[label="",style="solid", color="burlywood", weight=3];
123[label="vz4/[]",fontsize=10,color="white",style="solid",shape="box"];4 -> 123[label="",style="solid", color="burlywood", weight=9];
123 -> 6[label="",style="solid", color="burlywood", weight=3];
5[label="filterM vz3 (vz40 : vz41)\n  Monad a",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="filterM vz3 []\n  Monad a",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="vz3 vz40 >>= filterM1 vz3 vz41 vz40\n  Monad a",fontsize=16,color="blue",shape="box"];124[label=">>= :: (Maybe Bool) -> (Bool -> Maybe ([] a)) -> Maybe ([] a)",fontsize=10,color="white",style="solid",shape="box"];7 -> 124[label="",style="solid", color="blue", weight=9];
124 -> 9[label="",style="solid", color="blue", weight=3];
125[label=">>= :: (IO Bool) -> (Bool -> IO ([] a)) -> IO ([] a)",fontsize=10,color="white",style="solid",shape="box"];7 -> 125[label="",style="solid", color="blue", weight=9];
125 -> 10[label="",style="solid", color="blue", weight=3];
126[label=">>= :: ([] Bool) -> (Bool -> [] ([] a)) -> [] ([] a)",fontsize=10,color="white",style="solid",shape="box"];7 -> 126[label="",style="solid", color="blue", weight=9];
126 -> 11[label="",style="solid", color="blue", weight=3];
8[label="return []\n  Monad a",fontsize=16,color="blue",shape="box"];127[label="return :: ([] a) -> Maybe ([] a)",fontsize=10,color="white",style="solid",shape="box"];8 -> 127[label="",style="solid", color="blue", weight=9];
127 -> 12[label="",style="solid", color="blue", weight=3];
128[label="return :: ([] a) -> IO ([] a)",fontsize=10,color="white",style="solid",shape="box"];8 -> 128[label="",style="solid", color="blue", weight=9];
128 -> 13[label="",style="solid", color="blue", weight=3];
129[label="return :: ([] a) -> [] ([] a)",fontsize=10,color="white",style="solid",shape="box"];8 -> 129[label="",style="solid", color="blue", weight=9];
129 -> 14[label="",style="solid", color="blue", weight=3];
9 -> 15[label="",style="dashed", color="red", weight=0];
9[label="vz3 vz40 >>= filterM1 vz3 vz41 vz40",fontsize=16,color="magenta"];9 -> 16[label="",style="dashed", color="magenta", weight=3];
10[label="vz3 vz40 >>= filterM1 vz3 vz41 vz40",fontsize=16,color="black",shape="box"];10 -> 17[label="",style="solid", color="black", weight=3];
11 -> 18[label="",style="dashed", color="red", weight=0];
11[label="vz3 vz40 >>= filterM1 vz3 vz41 vz40",fontsize=16,color="magenta"];11 -> 19[label="",style="dashed", color="magenta", weight=3];
12[label="return []",fontsize=16,color="black",shape="box"];12 -> 20[label="",style="solid", color="black", weight=3];
13 -> 90[label="",style="dashed", color="red", weight=0];
13[label="return []",fontsize=16,color="magenta"];13 -> 91[label="",style="dashed", color="magenta", weight=3];
14 -> 115[label="",style="dashed", color="red", weight=0];
14[label="return []",fontsize=16,color="magenta"];14 -> 116[label="",style="dashed", color="magenta", weight=3];
16[label="vz3 vz40",fontsize=16,color="green",shape="box"];16 -> 23[label="",style="dashed", color="green", weight=3];
15[label="vz5 >>= filterM1 vz3 vz41 vz40",fontsize=16,color="burlywood",shape="triangle"];134[label="vz5/Nothing",fontsize=10,color="white",style="solid",shape="box"];15 -> 134[label="",style="solid", color="burlywood", weight=9];
134 -> 24[label="",style="solid", color="burlywood", weight=3];
135[label="vz5/Just vz50",fontsize=10,color="white",style="solid",shape="box"];15 -> 135[label="",style="solid", color="burlywood", weight=9];
135 -> 25[label="",style="solid", color="burlywood", weight=3];
17[label="primbindIO (vz3 vz40) (filterM1 vz3 vz41 vz40)",fontsize=16,color="black",shape="box"];17 -> 26[label="",style="solid", color="black", weight=3];
19[label="vz3 vz40",fontsize=16,color="green",shape="box"];19 -> 30[label="",style="dashed", color="green", weight=3];
18[label="vz6 >>= filterM1 vz3 vz41 vz40",fontsize=16,color="burlywood",shape="triangle"];136[label="vz6/vz60 : vz61",fontsize=10,color="white",style="solid",shape="box"];18 -> 136[label="",style="solid", color="burlywood", weight=9];
136 -> 28[label="",style="solid", color="burlywood", weight=3];
137[label="vz6/[]",fontsize=10,color="white",style="solid",shape="box"];18 -> 137[label="",style="solid", color="burlywood", weight=9];
137 -> 29[label="",style="solid", color="burlywood", weight=3];
20[label="Just []",fontsize=16,color="green",shape="box"];91[label="[]",fontsize=16,color="green",shape="box"];90[label="return vz15",fontsize=16,color="black",shape="triangle"];90 -> 93[label="",style="solid", color="black", weight=3];
116[label="[]",fontsize=16,color="green",shape="box"];115[label="return vz16",fontsize=16,color="black",shape="triangle"];115 -> 118[label="",style="solid", color="black", weight=3];
23[label="vz40",fontsize=16,color="green",shape="box"];24[label="Nothing >>= filterM1 vz3 vz41 vz40",fontsize=16,color="black",shape="box"];24 -> 32[label="",style="solid", color="black", weight=3];
25[label="Just vz50 >>= filterM1 vz3 vz41 vz40",fontsize=16,color="black",shape="box"];25 -> 33[label="",style="solid", color="black", weight=3];
26[label="terminator (vz3 vz40) (filterM1 vz3 vz41 vz40)",fontsize=16,color="black",shape="box"];26 -> 34[label="",style="solid", color="black", weight=3];
30[label="vz40",fontsize=16,color="green",shape="box"];28[label="vz60 : vz61 >>= filterM1 vz3 vz41 vz40",fontsize=16,color="black",shape="box"];28 -> 35[label="",style="solid", color="black", weight=3];
29[label="[] >>= filterM1 vz3 vz41 vz40",fontsize=16,color="black",shape="box"];29 -> 36[label="",style="solid", color="black", weight=3];
93[label="primretIO vz15",fontsize=16,color="black",shape="box"];93 -> 98[label="",style="solid", color="black", weight=3];
118[label="vz16 : []",fontsize=16,color="green",shape="box"];32[label="Nothing",fontsize=16,color="green",shape="box"];33[label="filterM1 vz3 vz41 vz40 vz50",fontsize=16,color="black",shape="box"];33 -> 38[label="",style="solid", color="black", weight=3];
34[label="ter0m (vz3 vz40) (filterM1 vz3 vz41 vz40)",fontsize=16,color="green",shape="box"];34 -> 39[label="",style="dashed", color="green", weight=3];
34 -> 40[label="",style="dashed", color="green", weight=3];
35 -> 41[label="",style="dashed", color="red", weight=0];
35[label="filterM1 vz3 vz41 vz40 vz60 ++ (vz61 >>= filterM1 vz3 vz41 vz40)",fontsize=16,color="magenta"];35 -> 42[label="",style="dashed", color="magenta", weight=3];
36[label="[]",fontsize=16,color="green",shape="box"];98[label="terminator vz15",fontsize=16,color="black",shape="box"];98 -> 102[label="",style="solid", color="black", weight=3];
38 -> 44[label="",style="dashed", color="red", weight=0];
38[label="filterM vz3 vz41 >>= filterM0 vz50 vz40",fontsize=16,color="magenta"];38 -> 45[label="",style="dashed", color="magenta", weight=3];
39[label="vz3 vz40",fontsize=16,color="green",shape="box"];39 -> 46[label="",style="dashed", color="green", weight=3];
40[label="filterM1 vz3 vz41 vz40",fontsize=16,color="grey",shape="box"];40 -> 47[label="",style="dashed", color="grey", weight=3];
42 -> 18[label="",style="dashed", color="red", weight=0];
42[label="vz61 >>= filterM1 vz3 vz41 vz40",fontsize=16,color="magenta"];42 -> 48[label="",style="dashed", color="magenta", weight=3];
41[label="filterM1 vz3 vz41 vz40 vz60 ++ vz7",fontsize=16,color="black",shape="triangle"];41 -> 49[label="",style="solid", color="black", weight=3];
102[label="ter3m vz15",fontsize=16,color="green",shape="box"];102 -> 107[label="",style="dashed", color="green", weight=3];
45 -> 4[label="",style="dashed", color="red", weight=0];
45[label="filterM vz3 vz41",fontsize=16,color="magenta"];45 -> 50[label="",style="dashed", color="magenta", weight=3];
44[label="vz8 >>= filterM0 vz50 vz40",fontsize=16,color="burlywood",shape="triangle"];142[label="vz8/Nothing",fontsize=10,color="white",style="solid",shape="box"];44 -> 142[label="",style="solid", color="burlywood", weight=9];
142 -> 51[label="",style="solid", color="burlywood", weight=3];
143[label="vz8/Just vz80",fontsize=10,color="white",style="solid",shape="box"];44 -> 143[label="",style="solid", color="burlywood", weight=9];
143 -> 52[label="",style="solid", color="burlywood", weight=3];
46[label="vz40",fontsize=16,color="green",shape="box"];47[label="filterM1 vz3 vz41 vz40 vz9",fontsize=16,color="black",shape="triangle"];47 -> 53[label="",style="solid", color="black", weight=3];
48[label="vz61",fontsize=16,color="green",shape="box"];49 -> 54[label="",style="dashed", color="red", weight=0];
49[label="(filterM vz3 vz41 >>= filterM0 vz60 vz40) ++ vz7",fontsize=16,color="magenta"];49 -> 55[label="",style="dashed", color="magenta", weight=3];
107[label="vz15",fontsize=16,color="green",shape="box"];50[label="vz41",fontsize=16,color="green",shape="box"];51[label="Nothing >>= filterM0 vz50 vz40",fontsize=16,color="black",shape="box"];51 -> 56[label="",style="solid", color="black", weight=3];
52[label="Just vz80 >>= filterM0 vz50 vz40",fontsize=16,color="black",shape="box"];52 -> 57[label="",style="solid", color="black", weight=3];
53 -> 58[label="",style="dashed", color="red", weight=0];
53[label="filterM vz3 vz41 >>= filterM0 vz9 vz40",fontsize=16,color="magenta"];53 -> 59[label="",style="dashed", color="magenta", weight=3];
55 -> 4[label="",style="dashed", color="red", weight=0];
55[label="filterM vz3 vz41",fontsize=16,color="magenta"];55 -> 60[label="",style="dashed", color="magenta", weight=3];
54[label="(vz10 >>= filterM0 vz60 vz40) ++ vz7",fontsize=16,color="burlywood",shape="triangle"];147[label="vz10/vz100 : vz101",fontsize=10,color="white",style="solid",shape="box"];54 -> 147[label="",style="solid", color="burlywood", weight=9];
147 -> 61[label="",style="solid", color="burlywood", weight=3];
148[label="vz10/[]",fontsize=10,color="white",style="solid",shape="box"];54 -> 148[label="",style="solid", color="burlywood", weight=9];
148 -> 62[label="",style="solid", color="burlywood", weight=3];
56[label="Nothing",fontsize=16,color="green",shape="box"];57[label="filterM0 vz50 vz40 vz80",fontsize=16,color="black",shape="box"];57 -> 63[label="",style="solid", color="black", weight=3];
59 -> 4[label="",style="dashed", color="red", weight=0];
59[label="filterM vz3 vz41",fontsize=16,color="magenta"];59 -> 64[label="",style="dashed", color="magenta", weight=3];
58[label="vz11 >>= filterM0 vz9 vz40",fontsize=16,color="black",shape="triangle"];58 -> 65[label="",style="solid", color="black", weight=3];
60[label="vz41",fontsize=16,color="green",shape="box"];61[label="(vz100 : vz101 >>= filterM0 vz60 vz40) ++ vz7",fontsize=16,color="black",shape="box"];61 -> 66[label="",style="solid", color="black", weight=3];
62[label="([] >>= filterM0 vz60 vz40) ++ vz7",fontsize=16,color="black",shape="box"];62 -> 67[label="",style="solid", color="black", weight=3];
63[label="return (filterM00 vz40 vz80 vz50)",fontsize=16,color="black",shape="box"];63 -> 68[label="",style="solid", color="black", weight=3];
64[label="vz41",fontsize=16,color="green",shape="box"];65[label="primbindIO vz11 (filterM0 vz9 vz40)",fontsize=16,color="black",shape="box"];65 -> 69[label="",style="solid", color="black", weight=3];
66[label="(filterM0 vz60 vz40 vz100 ++ (vz101 >>= filterM0 vz60 vz40)) ++ vz7",fontsize=16,color="black",shape="box"];66 -> 70[label="",style="solid", color="black", weight=3];
67[label="[] ++ vz7",fontsize=16,color="black",shape="triangle"];67 -> 71[label="",style="solid", color="black", weight=3];
68[label="Just (filterM00 vz40 vz80 vz50)",fontsize=16,color="green",shape="box"];68 -> 72[label="",style="dashed", color="green", weight=3];
69[label="terminator vz11 (filterM0 vz9 vz40)",fontsize=16,color="black",shape="box"];69 -> 73[label="",style="solid", color="black", weight=3];
70[label="(return (filterM00 vz40 vz100 vz60) ++ (vz101 >>= filterM0 vz60 vz40)) ++ vz7",fontsize=16,color="black",shape="box"];70 -> 74[label="",style="solid", color="black", weight=3];
71[label="vz7",fontsize=16,color="green",shape="box"];72[label="filterM00 vz40 vz80 vz50",fontsize=16,color="burlywood",shape="triangle"];150[label="vz50/False",fontsize=10,color="white",style="solid",shape="box"];72 -> 150[label="",style="solid", color="burlywood", weight=9];
150 -> 75[label="",style="solid", color="burlywood", weight=3];
151[label="vz50/True",fontsize=10,color="white",style="solid",shape="box"];72 -> 151[label="",style="solid", color="burlywood", weight=9];
151 -> 76[label="",style="solid", color="burlywood", weight=3];
73[label="ter2m vz11 (filterM0 vz9 vz40)",fontsize=16,color="green",shape="box"];73 -> 77[label="",style="dashed", color="green", weight=3];
73 -> 78[label="",style="dashed", color="green", weight=3];
74 -> 79[label="",style="dashed", color="red", weight=0];
74[label="((filterM00 vz40 vz100 vz60 : []) ++ (vz101 >>= filterM0 vz60 vz40)) ++ vz7",fontsize=16,color="magenta"];74 -> 80[label="",style="dashed", color="magenta", weight=3];
75[label="filterM00 vz40 vz80 False",fontsize=16,color="black",shape="box"];75 -> 81[label="",style="solid", color="black", weight=3];
76[label="filterM00 vz40 vz80 True",fontsize=16,color="black",shape="box"];76 -> 82[label="",style="solid", color="black", weight=3];
77[label="vz11",fontsize=16,color="green",shape="box"];78[label="filterM0 vz9 vz40",fontsize=16,color="grey",shape="box"];78 -> 83[label="",style="dashed", color="grey", weight=3];
80 -> 72[label="",style="dashed", color="red", weight=0];
80[label="filterM00 vz40 vz100 vz60",fontsize=16,color="magenta"];80 -> 84[label="",style="dashed", color="magenta", weight=3];
80 -> 85[label="",style="dashed", color="magenta", weight=3];
79[label="((vz12 : []) ++ (vz101 >>= filterM0 vz60 vz40)) ++ vz7",fontsize=16,color="black",shape="triangle"];79 -> 86[label="",style="solid", color="black", weight=3];
81[label="vz80",fontsize=16,color="green",shape="box"];82[label="vz40 : vz80",fontsize=16,color="green",shape="box"];83[label="filterM0 vz9 vz40 vz13",fontsize=16,color="black",shape="triangle"];83 -> 87[label="",style="solid", color="black", weight=3];
84[label="vz60",fontsize=16,color="green",shape="box"];85[label="vz100",fontsize=16,color="green",shape="box"];86 -> 88[label="",style="dashed", color="red", weight=0];
86[label="(vz12 : [] ++ (vz101 >>= filterM0 vz60 vz40)) ++ vz7",fontsize=16,color="magenta"];86 -> 89[label="",style="dashed", color="magenta", weight=3];
87 -> 90[label="",style="dashed", color="red", weight=0];
87[label="return (filterM00 vz40 vz13 vz9)",fontsize=16,color="magenta"];87 -> 92[label="",style="dashed", color="magenta", weight=3];
89 -> 67[label="",style="dashed", color="red", weight=0];
89[label="[] ++ (vz101 >>= filterM0 vz60 vz40)",fontsize=16,color="magenta"];89 -> 94[label="",style="dashed", color="magenta", weight=3];
88[label="(vz12 : vz14) ++ vz7",fontsize=16,color="black",shape="triangle"];88 -> 95[label="",style="solid", color="black", weight=3];
92 -> 72[label="",style="dashed", color="red", weight=0];
92[label="filterM00 vz40 vz13 vz9",fontsize=16,color="magenta"];92 -> 96[label="",style="dashed", color="magenta", weight=3];
92 -> 97[label="",style="dashed", color="magenta", weight=3];
94[label="vz101 >>= filterM0 vz60 vz40",fontsize=16,color="burlywood",shape="triangle"];158[label="vz101/vz1010 : vz1011",fontsize=10,color="white",style="solid",shape="box"];94 -> 158[label="",style="solid", color="burlywood", weight=9];
158 -> 99[label="",style="solid", color="burlywood", weight=3];
159[label="vz101/[]",fontsize=10,color="white",style="solid",shape="box"];94 -> 159[label="",style="solid", color="burlywood", weight=9];
159 -> 100[label="",style="solid", color="burlywood", weight=3];
95[label="vz12 : vz14 ++ vz7",fontsize=16,color="green",shape="box"];95 -> 101[label="",style="dashed", color="green", weight=3];
96[label="vz9",fontsize=16,color="green",shape="box"];97[label="vz13",fontsize=16,color="green",shape="box"];99[label="vz1010 : vz1011 >>= filterM0 vz60 vz40",fontsize=16,color="black",shape="box"];99 -> 103[label="",style="solid", color="black", weight=3];
100[label="[] >>= filterM0 vz60 vz40",fontsize=16,color="black",shape="box"];100 -> 104[label="",style="solid", color="black", weight=3];
101[label="vz14 ++ vz7",fontsize=16,color="burlywood",shape="triangle"];160[label="vz14/vz140 : vz141",fontsize=10,color="white",style="solid",shape="box"];101 -> 160[label="",style="solid", color="burlywood", weight=9];
160 -> 105[label="",style="solid", color="burlywood", weight=3];
161[label="vz14/[]",fontsize=10,color="white",style="solid",shape="box"];101 -> 161[label="",style="solid", color="burlywood", weight=9];
161 -> 106[label="",style="solid", color="burlywood", weight=3];
103 -> 101[label="",style="dashed", color="red", weight=0];
103[label="filterM0 vz60 vz40 vz1010 ++ (vz1011 >>= filterM0 vz60 vz40)",fontsize=16,color="magenta"];103 -> 108[label="",style="dashed", color="magenta", weight=3];
103 -> 109[label="",style="dashed", color="magenta", weight=3];
104[label="[]",fontsize=16,color="green",shape="box"];105[label="(vz140 : vz141) ++ vz7",fontsize=16,color="black",shape="box"];105 -> 110[label="",style="solid", color="black", weight=3];
106[label="[] ++ vz7",fontsize=16,color="black",shape="box"];106 -> 111[label="",style="solid", color="black", weight=3];
108 -> 94[label="",style="dashed", color="red", weight=0];
108[label="vz1011 >>= filterM0 vz60 vz40",fontsize=16,color="magenta"];108 -> 112[label="",style="dashed", color="magenta", weight=3];
109[label="filterM0 vz60 vz40 vz1010",fontsize=16,color="black",shape="box"];109 -> 113[label="",style="solid", color="black", weight=3];
110[label="vz140 : vz141 ++ vz7",fontsize=16,color="green",shape="box"];110 -> 114[label="",style="dashed", color="green", weight=3];
111[label="vz7",fontsize=16,color="green",shape="box"];112[label="vz1011",fontsize=16,color="green",shape="box"];113 -> 115[label="",style="dashed", color="red", weight=0];
113[label="return (filterM00 vz40 vz1010 vz60)",fontsize=16,color="magenta"];113 -> 117[label="",style="dashed", color="magenta", weight=3];
114 -> 101[label="",style="dashed", color="red", weight=0];
114[label="vz141 ++ vz7",fontsize=16,color="magenta"];114 -> 119[label="",style="dashed", color="magenta", weight=3];
117 -> 72[label="",style="dashed", color="red", weight=0];
117[label="filterM00 vz40 vz1010 vz60",fontsize=16,color="magenta"];117 -> 120[label="",style="dashed", color="magenta", weight=3];
117 -> 121[label="",style="dashed", color="magenta", weight=3];
119[label="vz141",fontsize=16,color="green",shape="box"];120[label="vz60",fontsize=16,color="green",shape="box"];121[label="vz1010",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(vz140, vz141), vz7, h) → new_psPs(vz141, vz7, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_psPs(:(vz140, vz141), vz7, h) → new_psPs(vz141, vz7, h)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs(:(vz1010, vz1011), vz60, vz40, h) → new_gtGtEs(vz1011, vz60, vz40, h)

From the DPs we obtained the following set of size-change graphs:

new_gtGtEs(:(vz1010, vz1011), vz60, vz40, h) → new_gtGtEs(vz1011, vz60, vz40, h)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_[], h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_psPs0(vz3, vz41, vz40, h)
new_filterM(vz3, :(vz40, vz41), ty_IO, h) → new_filterM(vz3, vz41, ty_IO, h)
new_filterM(vz3, :(vz40, vz41), ty_[], h) → new_gtGtEs1(vz3, vz41, vz40, h)
new_filterM(vz3, :(vz40, vz41), ty_Maybe, h) → new_gtGtEs0(vz3, vz41, vz40, h)
new_filterM1(vz3, vz41, vz40, vz9, h) → new_filterM(vz3, vz41, ty_IO, h)
new_gtGtEs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_Maybe, h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_gtGtEs1(vz3, vz41, vz40, h)

The TRS R consists of the following rules:

new_psPs6([], vz60, vz40, vz7, h) → new_psPs4(vz7, h)
new_psPs5(vz3, vz41, vz40, vz60, vz7, h) → new_psPs6(new_filterM0(vz3, vz41, ty_[], h), vz60, vz40, vz7, h)
new_psPs2(vz12, vz101, vz60, vz40, vz7, h) → new_psPs3(vz12, new_psPs4(new_gtGtEs3(vz101, vz60, vz40, h), h), vz7, h)
new_filterM00(vz40, vz80, False, h) → vz80
new_gtGtEs2(:(vz60, vz61), vz3, vz41, vz40, h) → new_psPs5(vz3, vz41, vz40, vz60, new_gtGtEs2(vz61, vz3, vz41, vz40, h), h)
new_return(vz16, h) → :(vz16, [])
new_filterM00(vz40, vz80, True, h) → :(vz40, vz80)
new_psPs4(vz7, h) → vz7
new_gtGtEs3(:(vz1010, vz1011), vz60, vz40, h) → new_psPs1(new_return(new_filterM00(vz40, vz1010, vz60, h), h), new_gtGtEs3(vz1011, vz60, vz40, h), h)
new_psPs1([], vz7, h) → vz7
new_psPs6(:(vz100, vz101), vz60, vz40, vz7, h) → new_psPs2(new_filterM00(vz40, vz100, vz60, h), vz101, vz60, vz40, vz7, h)
new_gtGtEs2([], vz3, vz41, vz40, h) → []
new_psPs3(vz12, vz14, vz7, h) → :(vz12, new_psPs1(vz14, vz7, h))
new_gtGtEs3([], vz60, vz40, h) → []
new_psPs1(:(vz140, vz141), vz7, h) → :(vz140, new_psPs1(vz141, vz7, h))

The set Q consists of the following terms:

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                            ↳ QDP

                            ↳ QDP

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_filterM(vz3, :(vz40, vz41), ty_Maybe, h) → new_gtGtEs0(vz3, vz41, vz40, h)
new_gtGtEs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_Maybe, h)

The TRS R consists of the following rules:

new_psPs6([], vz60, vz40, vz7, h) → new_psPs4(vz7, h)
new_psPs5(vz3, vz41, vz40, vz60, vz7, h) → new_psPs6(new_filterM0(vz3, vz41, ty_[], h), vz60, vz40, vz7, h)
new_psPs2(vz12, vz101, vz60, vz40, vz7, h) → new_psPs3(vz12, new_psPs4(new_gtGtEs3(vz101, vz60, vz40, h), h), vz7, h)
new_filterM00(vz40, vz80, False, h) → vz80
new_gtGtEs2(:(vz60, vz61), vz3, vz41, vz40, h) → new_psPs5(vz3, vz41, vz40, vz60, new_gtGtEs2(vz61, vz3, vz41, vz40, h), h)
new_return(vz16, h) → :(vz16, [])
new_filterM00(vz40, vz80, True, h) → :(vz40, vz80)
new_psPs4(vz7, h) → vz7
new_gtGtEs3(:(vz1010, vz1011), vz60, vz40, h) → new_psPs1(new_return(new_filterM00(vz40, vz1010, vz60, h), h), new_gtGtEs3(vz1011, vz60, vz40, h), h)
new_psPs1([], vz7, h) → vz7
new_psPs6(:(vz100, vz101), vz60, vz40, vz7, h) → new_psPs2(new_filterM00(vz40, vz100, vz60, h), vz101, vz60, vz40, vz7, h)
new_gtGtEs2([], vz3, vz41, vz40, h) → []
new_psPs3(vz12, vz14, vz7, h) → :(vz12, new_psPs1(vz14, vz7, h))
new_gtGtEs3([], vz60, vz40, h) → []
new_psPs1(:(vz140, vz141), vz7, h) → :(vz140, new_psPs1(vz141, vz7, h))

The set Q consists of the following terms:

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                            ↳ QDP

                            ↳ QDP

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_filterM(vz3, :(vz40, vz41), ty_Maybe, h) → new_gtGtEs0(vz3, vz41, vz40, h)
new_gtGtEs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_Maybe, h)

R is empty.
The set Q consists of the following terms:

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ QDPSizeChangeProof

                            ↳ QDP

                            ↳ QDP

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_filterM(vz3, :(vz40, vz41), ty_Maybe, h) → new_gtGtEs0(vz3, vz41, vz40, h)
new_gtGtEs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_Maybe, h)

From the DPs we obtained the following set of size-change graphs:

new_gtGtEs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_Maybe, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 4
new_filterM(vz3, :(vz40, vz41), ty_Maybe, h) → new_gtGtEs0(vz3, vz41, vz40, h)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 4 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                            ↳ QDP

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_filterM(vz3, :(vz40, vz41), ty_IO, h) → new_filterM(vz3, vz41, ty_IO, h)

The TRS R consists of the following rules:

new_psPs6([], vz60, vz40, vz7, h) → new_psPs4(vz7, h)
new_psPs5(vz3, vz41, vz40, vz60, vz7, h) → new_psPs6(new_filterM0(vz3, vz41, ty_[], h), vz60, vz40, vz7, h)
new_psPs2(vz12, vz101, vz60, vz40, vz7, h) → new_psPs3(vz12, new_psPs4(new_gtGtEs3(vz101, vz60, vz40, h), h), vz7, h)
new_filterM00(vz40, vz80, False, h) → vz80
new_gtGtEs2(:(vz60, vz61), vz3, vz41, vz40, h) → new_psPs5(vz3, vz41, vz40, vz60, new_gtGtEs2(vz61, vz3, vz41, vz40, h), h)
new_return(vz16, h) → :(vz16, [])
new_filterM00(vz40, vz80, True, h) → :(vz40, vz80)
new_psPs4(vz7, h) → vz7
new_gtGtEs3(:(vz1010, vz1011), vz60, vz40, h) → new_psPs1(new_return(new_filterM00(vz40, vz1010, vz60, h), h), new_gtGtEs3(vz1011, vz60, vz40, h), h)
new_psPs1([], vz7, h) → vz7
new_psPs6(:(vz100, vz101), vz60, vz40, vz7, h) → new_psPs2(new_filterM00(vz40, vz100, vz60, h), vz101, vz60, vz40, vz7, h)
new_gtGtEs2([], vz3, vz41, vz40, h) → []
new_psPs3(vz12, vz14, vz7, h) → :(vz12, new_psPs1(vz14, vz7, h))
new_gtGtEs3([], vz60, vz40, h) → []
new_psPs1(:(vz140, vz141), vz7, h) → :(vz140, new_psPs1(vz141, vz7, h))

The set Q consists of the following terms:

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                            ↳ QDP

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_filterM(vz3, :(vz40, vz41), ty_IO, h) → new_filterM(vz3, vz41, ty_IO, h)

R is empty.
The set Q consists of the following terms:

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ QDPSizeChangeProof

                            ↳ QDP

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_filterM(vz3, :(vz40, vz41), ty_IO, h) → new_filterM(vz3, vz41, ty_IO, h)

From the DPs we obtained the following set of size-change graphs:

new_filterM(vz3, :(vz40, vz41), ty_IO, h) → new_filterM(vz3, vz41, ty_IO, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_[], h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_psPs0(vz3, vz41, vz40, h)
new_filterM(vz3, :(vz40, vz41), ty_[], h) → new_gtGtEs1(vz3, vz41, vz40, h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_gtGtEs1(vz3, vz41, vz40, h)

The TRS R consists of the following rules:

new_psPs6([], vz60, vz40, vz7, h) → new_psPs4(vz7, h)
new_psPs5(vz3, vz41, vz40, vz60, vz7, h) → new_psPs6(new_filterM0(vz3, vz41, ty_[], h), vz60, vz40, vz7, h)
new_psPs2(vz12, vz101, vz60, vz40, vz7, h) → new_psPs3(vz12, new_psPs4(new_gtGtEs3(vz101, vz60, vz40, h), h), vz7, h)
new_filterM00(vz40, vz80, False, h) → vz80
new_gtGtEs2(:(vz60, vz61), vz3, vz41, vz40, h) → new_psPs5(vz3, vz41, vz40, vz60, new_gtGtEs2(vz61, vz3, vz41, vz40, h), h)
new_return(vz16, h) → :(vz16, [])
new_filterM00(vz40, vz80, True, h) → :(vz40, vz80)
new_psPs4(vz7, h) → vz7
new_gtGtEs3(:(vz1010, vz1011), vz60, vz40, h) → new_psPs1(new_return(new_filterM00(vz40, vz1010, vz60, h), h), new_gtGtEs3(vz1011, vz60, vz40, h), h)
new_psPs1([], vz7, h) → vz7
new_psPs6(:(vz100, vz101), vz60, vz40, vz7, h) → new_psPs2(new_filterM00(vz40, vz100, vz60, h), vz101, vz60, vz40, vz7, h)
new_gtGtEs2([], vz3, vz41, vz40, h) → []
new_psPs3(vz12, vz14, vz7, h) → :(vz12, new_psPs1(vz14, vz7, h))
new_gtGtEs3([], vz60, vz40, h) → []
new_psPs1(:(vz140, vz141), vz7, h) → :(vz140, new_psPs1(vz141, vz7, h))

The set Q consists of the following terms:

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_[], h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_psPs0(vz3, vz41, vz40, h)
new_filterM(vz3, :(vz40, vz41), ty_[], h) → new_gtGtEs1(vz3, vz41, vz40, h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_gtGtEs1(vz3, vz41, vz40, h)

R is empty.
The set Q consists of the following terms:

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_psPs4(x0, x1)
new_psPs1([], x0, x1)
new_gtGtEs3(:(x0, x1), x2, x3, x4)
new_filterM00(x0, x1, True, x2)
new_psPs6([], x0, x1, x2, x3)
new_filterM00(x0, x1, False, x2)
new_gtGtEs2([], x0, x1, x2, x3)
new_gtGtEs3([], x0, x1, x2)
new_return(x0, x1)
new_psPs2(x0, x1, x2, x3, x4, x5)
new_gtGtEs2(:(x0, x1), x2, x3, x4, x5)
new_psPs5(x0, x1, x2, x3, x4, x5)
new_psPs3(x0, x1, x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_psPs6(:(x0, x1), x2, x3, x4, x5)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ UsableRulesReductionPairsProof

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_[], h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_psPs0(vz3, vz41, vz40, h)
new_filterM(vz3, :(vz40, vz41), ty_[], h) → new_gtGtEs1(vz3, vz41, vz40, h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_gtGtEs1(vz3, vz41, vz40, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

new_psPs0(vz3, vz41, vz40, h) → new_filterM(vz3, vz41, ty_[], h)
new_filterM(vz3, :(vz40, vz41), ty_[], h) → new_gtGtEs1(vz3, vz41, vz40, h)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(new_filterM(x₁, x₂, x₃, x₄)) = x₁ + 2·x₂ + 2·x₃ + x₄
POL(new_gtGtEs1(x₁, x₂, x₃, x₄)) = 1 + x₁ + 2·x₂ + x₃ + x₄
POL(new_psPs0(x₁, x₂, x₃, x₄)) = 1 + x₁ + 2·x₂ + x₃ + x₄
POL(ty_[]) = 0

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ UsableRulesReductionPairsProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs1(vz3, vz41, vz40, h) → new_psPs0(vz3, vz41, vz40, h)
new_gtGtEs1(vz3, vz41, vz40, h) → new_gtGtEs1(vz3, vz41, vz40, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ UsableRulesReductionPairsProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ NonTerminationProof

                  ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs1(vz3, vz41, vz40, h) → new_gtGtEs1(vz3, vz41, vz40, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_gtGtEs1(vz3, vz41, vz40, h) → new_gtGtEs1(vz3, vz41, vz40, h)

The TRS R consists of the following rules:none

s = new_gtGtEs1(vz3, vz41, vz40, h) evaluates to t =new_gtGtEs1(vz3, vz41, vz40, h)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_gtGtEs1(vz3, vz41, vz40, h) to new_gtGtEs1(vz3, vz41, vz40, h).

Haskell To QDPs